<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>13. Integration and Measure Theory &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="Index" href="genindex.html" />
    <link rel="prev" title="12. Differential Calculus" href="C12_Differential_Calculus.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">13. Integration and Measure Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#elementary-integration">13.1. Elementary Integration</a></li>
<li class="toctree-l2"><a class="reference internal" href="#measure-theory">13.2. Measure Theory</a></li>
<li class="toctree-l2"><a class="reference internal" href="#integration">13.3. Integration</a></li>
</ul>
</li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">13. </span>Integration and Measure Theory</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C13_Integration_and_Measure_Theory.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="index-0">
<span id="integration-and-measure-theory"></span><span id="id1"></span><h1><span class="section-number">13. </span>Integration and Measure Theory<a class="headerlink" href="#index-0" title="Link to this heading">&#61633;</a></h1>
<section id="elementary-integration">
<span id="index-1"></span><span id="id2"></span><h2><span class="section-number">13.1. </span>Elementary Integration<a class="headerlink" href="#elementary-integration" title="Link to this heading">&#61633;</a></h2>
<p>We first focus on integration of functions on finite intervals in <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>. We can integrate
elementary functions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MeasureTheory</span><span class="w"> </span><span class="n">intervalIntegral</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Interval</span>
<span class="c1">-- this introduces the notation `[[a, b]]` for the segment from `min a b` to `max a b`</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">a</span><span class="bp">..</span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_id</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8713;</span><span class="w"> </span><span class="o">[[</span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">b</span><span class="o">]])</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">a</span><span class="bp">..</span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Real.log</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_one_div</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The fundamental theorem of calculus relates integration and differentiation.
Below we give simplified statements of the two parts of this theorem. The first part
says that integration provides an inverse to differentiation and the second one
specifies how to compute integrals of derivatives.
(These two parts are very closely related, but their optimal versions,
which are not shown here, are not equivalent.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">a</span><span class="bp">..</span><span class="n">u</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">integral_hasStrictDerivAt_right</span><span class="w"> </span><span class="o">(</span><span class="n">hf.intervalIntegrable</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hf.stronglyMeasurableAtFilter</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span>
<span class="w">        </span><span class="n">hf.continuousAt</span><span class="o">)</span><span class="bp">.</span><span class="n">hasDerivAt.deriv</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">[[</span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">b</span><span class="o">]],</span><span class="w"> </span><span class="n">HasDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IntervalIntegrable</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">volume</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">a</span><span class="bp">..</span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_eq_sub_of_hasDerivAt</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#39;</span>
</pre></div>
</div>
<p>Convolution is also defined in Mathlib and its basic properties are proved.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Convolution</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8902;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">t</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
</section>
<section id="measure-theory">
<span id="index-2"></span><span id="id3"></span><h2><span class="section-number">13.2. </span>Measure Theory<a class="headerlink" href="#measure-theory" title="Link to this heading">&#61633;</a></h2>
<p>The general context for integration in Mathlib is measure theory. Even the elementary
integrals of the previous section are in fact Bochner integrals. Bochner integration is
a generalization of Lebesgue integration where the target space can be any Banach space,
not necessarily finite dimensional.</p>
<p>The first component in the development of measure theory
is the notion of a <span class="math notranslate nohighlight">\(\sigma\)</span>-algebra of sets, which are called the
<em>measurable</em> sets.
The type class <code class="docutils literal notranslate"><span class="pre">MeasurableSpace</span></code> serves to equip a type with such a structure.
The sets <code class="docutils literal notranslate"><span class="pre">empty</span></code> and <code class="docutils literal notranslate"><span class="pre">univ</span></code> are measurable,
the complement of a measurable set is measurable,
and a countable union or intersection of measurable sets is measurable.
Note that these axioms are redundant; if you <code class="docutils literal notranslate"><span class="pre">#print</span> <span class="pre">MeasurableSpace</span></code>,
you will see the ones that Mathlib uses.
As the examples below show, countability assumptions can be expressed using the
<code class="docutils literal notranslate"><span class="pre">Encodable</span></code> type class.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">MeasurableSpace</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8709;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MeasurableSet.empty</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="n">univ</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MeasurableSet.univ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="bp">&#7580;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hs.compl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Encodable</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Encodable</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Encodable</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8899;</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MeasurableSet.iUnion</span><span class="w"> </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8898;</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MeasurableSet.iInter</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>Once a type is measurable, we can measure it. On paper, a measure on a set
(or type) equipped with a
<span class="math notranslate nohighlight">\(\sigma\)</span>-algebra is a function from the measurable sets to
the extended non-negative reals that is
additive on countable disjoint unions.
In Mathlib, we don&#8217;t want to carry around measurability assumptions
every time we write an application of the measure to a set.
So we extend the measure to any set <code class="docutils literal notranslate"><span class="pre">s</span></code>
as the infimum of measures of measurable sets containing <code class="docutils literal notranslate"><span class="pre">s</span></code>.
Of course, many lemmas still require
measurability assumptions, but not all.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MeasureTheory</span><span class="w"> </span><span class="n">Function</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Measure</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="o">(</span><span class="n">t</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">_</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">_</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="n">t</span><span class="o">),</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">measure_eq_iInf</span><span class="w"> </span><span class="n">s</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8899;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8721;&#39;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">measure_iUnion_le</span><span class="w"> </span><span class="n">s</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hmeas</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">))</span><span class="w"> </span><span class="o">(</span><span class="n">hdis</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Pairwise</span><span class="w"> </span><span class="o">(</span><span class="n">Disjoint</span><span class="w"> </span><span class="n">on</span><span class="w"> </span><span class="n">f</span><span class="o">))</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">&#956;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8899;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;&#39;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#956;.m_iUnion</span><span class="w"> </span><span class="n">hmeas</span><span class="w"> </span><span class="n">hdis</span>
</pre></div>
</div>
<p>Once a type has a measure associated with it, we say that a property <code class="docutils literal notranslate"><span class="pre">P</span></code>
holds <em>almost everywhere</em> if the set of elements where the property fails
has measure 0.
The collection of properties that hold almost everywhere form a filter,
but Mathlib introduces special notation for saying that a property holds
almost everywhere.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Prop</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8704;&#7504;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="o">,</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">ae</span><span class="w"> </span><span class="n">&#956;</span><span class="o">,</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Iff.rfl</span>
</pre></div>
</div>
</section>
<section id="integration">
<span id="id4"></span><h2><span class="section-number">13.3. </span>Integration<a class="headerlink" href="#integration" title="Link to this heading">&#61633;</a></h2>
<p>Now that we have measurable spaces and measures we can consider integrals.
As explained above, Mathlib uses a very general notion of
integration that allows any Banach space as the target.
As usual, we don&#8217;t want our notation to
carry around assumptions, so we define integration in such a way
that an integral is equal to zero if the function in question is
not integrable.
Most lemmas having to do with integrals have integrability assumptions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Integrable</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">&#956;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Integrable</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">&#956;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_add</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">hg</span>
</pre></div>
</div>
<p>As an example of the complex interactions between our various conventions, let us see how to integrate constant functions.
Recall that a measure <code class="docutils literal notranslate"><span class="pre">&#956;</span></code> takes values in <code class="docutils literal notranslate"><span class="pre">&#8477;&#8805;0&#8734;</span></code>, the type of extended non-negative reals.
There is a function <code class="docutils literal notranslate"><span class="pre">ENNReal.toReal</span> <span class="pre">:</span> <span class="pre">&#8477;&#8805;0&#8734;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> which sends <code class="docutils literal notranslate"><span class="pre">&#8868;</span></code>,
the point at infinity, to zero.
For any <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">&#945;</span></code>, if <code class="docutils literal notranslate"><span class="pre">&#956;</span> <span class="pre">s</span> <span class="pre">=</span> <span class="pre">&#8868;</span></code>, then nonzero constant functions are not integrable on <code class="docutils literal notranslate"><span class="pre">s</span></code>.
In that case, their integrals are equal to zero by definition, as is <code class="docutils literal notranslate"><span class="pre">(&#956;</span> <span class="pre">s).toReal</span></code>.
So in all cases we have the following lemma.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">&#956;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="bp">.</span><span class="n">toReal</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">setIntegral_const</span><span class="w"> </span><span class="n">c</span>
</pre></div>
</div>
<p>We now quickly explain how to access the most important theorems in integration theory, starting
with the dominated convergence theorem. There are several versions in Mathlib,
and here we only show the most basic one.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Filter</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">bound</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hmeas</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">AEStronglyMeasurable</span><span class="w"> </span><span class="o">(</span><span class="n">F</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="n">&#956;</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hint</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Integrable</span><span class="w"> </span><span class="n">bound</span><span class="w"> </span><span class="n">&#956;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hbound</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;&#7504;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">F</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">a</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">bound</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hlim</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;&#7504;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="o">,</span><span class="w"> </span><span class="n">Tendsto</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="n">atTop</span><span class="w"> </span><span class="o">(</span><span class="n">&#120029;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)))</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Tendsto</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="o">)</span><span class="w"> </span><span class="n">atTop</span><span class="w"> </span><span class="o">(</span><span class="n">&#120029;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">tendsto_integral_of_dominated_convergence</span><span class="w"> </span><span class="n">bound</span><span class="w"> </span><span class="n">hmeas</span><span class="w"> </span><span class="n">hint</span><span class="w"> </span><span class="n">hbound</span><span class="w"> </span><span class="n">hlim</span>
</pre></div>
</div>
<p>Then we have Fubini&#8217;s theorem for integrals on product type.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">MeasurableSpace</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Measure</span><span class="w"> </span><span class="n">&#945;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">SigmaFinite</span><span class="w"> </span><span class="n">&#956;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">&#946;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">MeasurableSpace</span><span class="w"> </span><span class="n">&#946;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">&#957;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Measure</span><span class="w"> </span><span class="n">&#946;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">SigmaFinite</span><span class="w"> </span><span class="n">&#957;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Integrable</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">&#956;.prod</span><span class="w"> </span><span class="n">&#957;</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">z</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8706;</span><span class="w"> </span><span class="n">&#956;.prod</span><span class="w"> </span><span class="n">&#957;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#957;</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_prod</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hf</span>
</pre></div>
</div>
<p>There is a very general version of convolution that applies to any
continuous bilinear form.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Convolution</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MeasurableSpace</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">Sub</span><span class="w"> </span><span class="n">G</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E&#39;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">L</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">E&#39;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Measure</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8902;</span><span class="o">[</span><span class="n">L</span><span class="o">,</span><span class="w"> </span><span class="n">&#956;</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">t</span><span class="o">,</span><span class="w"> </span><span class="n">L</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">t</span><span class="o">))</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>Finally, Mathlib has a very general version of the change-of-variables formula.
In the statement below, <code class="docutils literal notranslate"><span class="pre">BorelSpace</span> <span class="pre">E</span></code> means the
<span class="math notranslate nohighlight">\(\sigma\)</span>-algebra on <code class="docutils literal notranslate"><span class="pre">E</span></code> is generated by the open sets of <code class="docutils literal notranslate"><span class="pre">E</span></code>,
and <code class="docutils literal notranslate"><span class="pre">IsAddHaarMeasure</span> <span class="pre">&#956;</span></code> means that the measure <code class="docutils literal notranslate"><span class="pre">&#956;</span></code> is left-invariant,
gives finite mass to compact sets, and give positive mass to open sets.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">    </span><span class="o">[</span><span class="n">MeasurableSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">BorelSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Measure</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">&#956;.IsAddHaarMeasure</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>
<span class="w">    </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#8477;</span><span class="o">]</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MeasurableSet</span><span class="w"> </span><span class="n">s</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">HasFDerivWithinAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h_inj</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">InjOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#39;&#39;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8747;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="bp">|</span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">det</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8706;</span><span class="n">&#956;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">integral_image_eq_integral_abs_det_fderiv_smul</span><span class="w"> </span><span class="n">&#956;</span><span class="w"> </span><span class="n">hs</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">h_inj</span><span class="w"> </span><span class="n">g</span>
</pre></div>
</div>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C12_Differential_Calculus.html" class="btn btn-neutral float-left" title="12. Differential Calculus" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="genindex.html" class="btn btn-neutral float-right" title="Index" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>